The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#less(@x, @y) → #cklt(#compare(@x, @y))
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(#less(@y, @x), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insert#2(#true, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insertD(@x, @l) → insertD#1(@l, @x)
insertD#1(::(@y, @ys), @x) → insertD#2(#less(@y, @x), @x, @y, @ys)
insertD#1(nil, @x) → ::(@x, nil)
insertD#2(#false, @x, @y, @ys) → ::(@x, ::(@y, @ys))
insertD#2(#true, @x, @y, @ys) → ::(@y, insertD(@x, @ys))
insertionsort(@l) → insertionsort#1(@l)
insertionsort#1(::(@x, @xs)) → insert(@x, insertionsort(@xs))
insertionsort#1(nil) → nil
insertionsortD(@l) → insertionsortD#1(@l)
insertionsortD#1(::(@x, @xs)) → insertD(@x, insertionsortD(@xs))
insertionsortD#1(nil) → nil
testInsertionsort(@x) → insertionsort(testList(#unit))
testInsertionsortD(@x) → insertionsortD(testList(#unit))
testList(@_) → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))

The (relative) TRS S consists of the following rules:

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
insert(#pos(@y5602_3), ::(#0, @ys5355_3)) →⁺ ::(#0, insert(#pos(@y5602_3), @ys5355_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@ys5355_3 / ::(#0, @ys5355_3)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)